TFP 2020 Accepted Papers with Abstracts

Abstract: Asynchronous concurrent programing is a widely spread technique offering some simple concurrent primitives that are restricted in such a way that the resulting concurrent programs are dead-lock free.

In this paper, we develop and study a formal model of the underlying application programmer interface. For such a purpose, we formally define the extension of a monad by some notion of monad references uniquely bound to running monad actions together with the associated asynchronous primitives fork and read. The expected semantics is specified via two series of equations relating the behavior of these extension primitives with the underlying monad primitives.

This allows for formally stating and proving various properties of the resulting model of asynchronous programing. As a particular case, we eventually recover the notion of promises and we formally prove that, under simple further restrictions, promises induce a monad isomorphic to the underlying monad. This also allows for lifting asynchronous concurrent programming to data-flow concurrent programing.

Our proposal is illustrated throughout by concrete extensions of Haskell IO monad that allows for assessing the validity of the proposed equations and for showing how closely our proposal is related with existing libraries.

Abstract: Type error messages of compilers of statically typed functional languages are often inaccurate, making type error debugging hard. Many solutions to the problem have been proposed, but most have been evaluated only with short programs, that is, of fewer than 30 lines. In this paper we note that our own tool for delta debugging type errors scales poorly for large real-world programs. In response we present a new tool that applies a new algorithm for segmenting a large program before the delta debugging algorithm is applied. We propose a framework for evaluating type error debuggers and apply it to our new tool, demonstrating substantial improvement.

Abstract: In this article we examine the computation order and consequent
performance of three different conceptual implementations of the
fold function. We explore a set of performance based
experiments on different implementations of this function. In
particular, we contrast the fold-left implementation with two
other implements we refer to as pair-wise-fold and
tree-like-fold. We explore two application areas: ratio
arithmetic and Binary Decisions Diagram construction. We demonstrate
several cases where the performance of certain algorithms is very
different depending on the approach taken. In particular iterative
computations where the object size accumulates are good candidates for
the tree-like-fold.

Abstract: This paper presents PaSe, an extensible and inspectable DSL embedded in Haskell for expressing micro-animations. The philosophy of PaSe is to compose animations based on sequential and parallel composition of smaller animations. This differs from other animation libraries that focus more on sequential composition and have only limited forms of parallel composition. To provide similar flexibility as other animation libraries, PaSe features extensibility of operations and inspectability of animations. We present the features of PaSe with a to-do list application, discuss the PaSe implementation, and argue that the callback style of extensibility is detrimental for correctly combining PaSe features. We contrast with the GreenSock Animation Platform, a professional-grade and widely used JavaScript animation library, to illustrate this point.

Abstract: Software that models business workflows is omnipresent in today's society.
These systems coordinate collaboration in hospitals, companies, and military institutions.
Unfortunately, workflow systems may obfuscate the influence of current user actions on the desired end result.
In order to make the right decision, users need to oversee the full process and all information available,
both of which are usually buried in the system.
We have developed a way to automatically generate next step hints for task oriented programs.
Task oriented programming provides programmers with an abstraction over workflow software, while still being expressive enough to describe real world collaboration.
By leveraging symbolic execution, we can calculate these hints without modification of the original program.
To our knowledge, this is the first time that symbolic execution is used to automatically generate next step hints for end users.
We prove the generated hints to be sound and complete,
and also demonstrate that the symbolic execution semantics we employ is correct for sequential input.
In addition, we have developed a Haskell implementation of our automatic next step hint generation system.
By providing next step hints, the chance of human error is reduced, while still allowing end users to intervene if required.
The overall performance is raised, since the quality of decisions will improve.

Abstract: Embedded Domain-Specific Languages (EDSLs) are an alternative to quickly implement specialized languages without the need to write compilers or interpreters from scratch. In this territory, Haskell is a prime choice as the host language. EDSLs in Haskell, however, are often incapable of reifying useful static information from the source code, namely variable binding names and source locations. Not having access to variable names directly affects EDSLs designed to generate low-level code, where the variables names in the generated code do not match those found in the source code—thus broadening the semantic gap among source and target code. Similarly, many existing EDSLs produce poor error messages due to the lack of knowledge of source locations where errors are generated.

In this work, we propose a simple technique for enhancing monadic EDSLs expressed using do notation. This technique employs source-to-source plugins, a relatively new feature of GHC, to annotate every do statement of our EDSLs with relevant information extracted from the source code at compile time. We show how these annotations can be incorporated into EDSL designs either directly inside values or as monadic effects. We provide BinderAnn, a GHC source plugin implementing our ideas, and evaluate it by enhancing existing real-world EDSLs with relatively minor modification efforts to contemplate the source-level static information related to variables names and source locations.

Abstract: Algebraic effects and handlers are an emerging new feature to model effectful computations and attract attention not only from researchers but also from programmers.
They are implemented in various ways as part of compilers, interpreters, or as libraries.
We present a direct embedding of one-shot algebraic effects and handlers in a language which has asymmetric coroutines.
The key observation is that, by restricting the use of continuations to be one-shot, we obtain a simple and sufficiently general implementation via coroutines, which are available in many modern programming languages.
We have implemented our embedding as a library in Lua and Ruby, which allows one to write effectful programs in a modular way using algebraic effects and handlers.

Abstract: Agile software development and Formal Methods are traditionally seen as being
in conflict. From an Agile perspective, there is
pressure to deliver quickly, building vertical prototypes and doing
many iterations / sprints, refining the requirements; from a Formal
Methods perspective, there is pressure to deliver correctly and any
change in requirements often necessitates changes in the formal specification
and might even impact all arguments of correctness.
These two goals are often discordant. In this paper, we argue that
given the right attitudes on both sides, it is possible to fuse good practices
from formal methods and agile software engineering to deliver software that is
simultaneously reliable, effective, testable, and that can also be delivered
rapidly.

This suggests a new lightweight software engineering methodology, that is
inspired by and exploits appropriate formal methods, while also providing the
benefits of agile software development. Our methodology is informed and
motivated by practical experience. We have devised and adapted it in the
light of experience in delivering a large-scale software system that needs to
meet complex real-world requirements: the Cardano crypto-currency.
Crypto-Currencies is a rather new application area for which no clear
engineering habit exists, so it is a fitting domain for agile methods. At the
same time, there is a lot of real monetary value at stake, making it a good
fit for using formal methods to ensure high quality and correctness. The paper
reports on the issues that have been faced and overcome, and provides a number
of real-world lessons that can be used in similar situations.

Abstract: The additional complexity of dividing the computations of parallel programs into parallelizable parts and mapping these parts onto the available processors asks for a structured solution.
Functional programming seems like an auspicious approach to control the additional complexity and numerous functional high-level approaches that reduce complexity exist.
Of all the different approaches to parallel programming the concept
of algorithmic skeletons is one of the most promising.
Not least
because skeletons are a known technique to achieve
modularity.
In this paper we extend algorithmic skeletons with Placement Strategies: a functional, structured mechanism to organize coordination of parallel computation placement. Placement Strategies allow to access (semi-)explicit placement in a functional style. By doing so we increase the flexibility and clarity of algorithmic skeletons.
Example skeletons are implemented using an extension of Eden's Remote Data, that allows for simple skeleton composition and drop-in parallelization of sequential programs.
Nevertheless the scheme of Placement Strategies is transferable to other functional languages that use explicit placement.
In experimental evaluation we will show the effectiveness of the new skeletons and that the overhead caused by the additional location information is marginal.

Abstract: Distributed systems programming exhibits a considerable degree of mostly-functional behaviour. On the other hand, programming every distributed system with no side-effect whatsoever is not realistic. Observational purity lends itself as a plausible alternative.

To exercise that choice for programming distributed systems, we present the λ(port) family of λ-Calculi. Ports and pure blocks are two characteristics of this family. Ports are the only single source of side-effects in the λ(port) family. Pure blocks are their linguistic support for declaring observational purity. Notably, pure blocks specify which nodes in the distributed system they are pure for. We promote a programming paradigm, in which, the programmer strives to maximise pure blocks and only leave the unavoidably effectful computations outside. Our paradigm brings added value to speculative execution, mock testing, distributed garbage collection, partial order reduction, and treatments of flaky tests.

We start the λ(port) family from its most basic member, in which messages are delivered instantly. We prove that observational equivalences of the more basic members of the family are retained upon addition of message delay, message loss, node failure, and network partitions. As such, one can freely prove observational equivalences in the most basic member without worrying about any of the successor features.

Abstract: The main strength of pure languages like Haskell is that
they allow a straightforward way of reasoning about programs called
equational reasoning. Gibbons and Hinze propose an axiomatic approach
for monadic equational reasoning which uses laws to characterise effects.
In this paper they show how the state monad and the nondeterminism
monad can be combined in one effect called backtrackable state (or “local
state”) and they illustrate how the two effects interact. A second way
for state and nondeterminism to interact is non-backtrackable state (or
“global state”) where state persists after backtracking. Pauwels et al.
show how backtrackable state can be simulated with non-backtrackable
state and prove correctness using the axiomatic approach proposed by
Gibbons and Hinze. Within this project we take this approach one step
further and simulate the backtrackable state (state and nondeterminism)
with only the state effect.

Abstract: Experiment-driven observation of the natural world is a key driver of scientific discovery and innovation. Yet, the growing technical complexity of experimental equipment has become a pressing problem that limits the number and diversity of experiments that can be performed, as well as the institutes and enterprises that can afford them. This project identifies an opportunity to increase the rate of discovery and innovation by lowering the threshold for experimentation, exemplified in the applications of fluorescence microscopy, a key approach in the life sciences. Our solution is an operational, deeply embedded domain-specific language (DSL) in Haskell. We aim to tackle this problem further by advancing the state-of-the-art in programming languages and knowledge representation to automate the equipment control and allow users to state what experiments they want to conduct, rather than how to perform them.

Abstract: We present an algorithm for generating paths through a set of mutually recursive functions. The algorithm is part of a tool for white-box test-case generation. While in imperative programs there is a well established notion of path depth, this is not the case in recursive programs. We define what we mean by path and path depth in these programs and propose an algorithm which generates all the static paths up to a given depth. When the algorithm is applied to iterative programs, the defined depth corresponds to the maximum number of iterations through any loop. When applied to non-tail recursive functions, the meaning is closely related to the maximum number of their unfoldings along the path. It can also be applied to hybrid programs where iteration and recursion are both present.

Abstract: Our research is part of a wider project that aims to investigate and reason about the correctness of scheme-based source code transformations on Erlang programs. In order to formally reason about the definition of a programming language and the software that has been built with it, we need a mathematically rigorous description of that language. In this paper, we present our proof-assistant-based formalisation of a subset of Erlang, intended to serve as a base for proving refactorings correct. After discussing how we reused concepts from related work, we show the syntax and semantics of our formal description, including the abstractions involved (e.g. closures). We also present essential properties of the formalisation (e.g. determinism) along with their machine-checked proofs. Finally, we prove the correctness of some simple refactoring strategies.

Abstract: Digital synthesis is a cross discipline application used in fields such as music,
telecommunication, and others. The nature of digital synthesis involving multiple tracks as
well as parallel post-processes lends itself naturally to the functional programming paradigm. The paper demonstrates this by creating a fully functional, cross platform, standalone
synthesizer application framework implemented in a pure lazy functional language. The
application handles MIDI input and produces wav output played by any multimedia player.
Therefore, it can serve as a preprocessor for users who intend to create digital signals
before transcribing them into a digital or physical media.

Abstract: We present an array comprehension language that features execution on single-instruction multiple-data (SIMD) architectures even in cases where a comprehension leads to certain kinds of non-regular nested parallelism. The comprehension language naturally supports features such as nesting, zipping, and filtering, and it also supports more advanced features such as sorting. We demonstrate how the language is compiled into efficient Futhark code featuring calls to the Futhark "segmented" library. Moreover, we give a number of examples showing that the array comprehension language provides the programmer with effective abstractions for expressing queries and computations to be executed on SIMD architectures, such as GPUs.

Abstract: For interactive systems it is often desirable that users can create tasks for the system dynamically. Often these tasks are internally specified by constrained types like Generalized DataTypes, GADTs, or function applications using typeclasses. For plain datatypes, or the corresponding functions, this is relative easy: the input can be captured by a structured editor or a simple parser from a textual input. However, in many situations such simple types are not enough. We either need GADTs or more constraints than can be checked by a parser.

To guarantee correct inputs we either need the invoke the compiler of the host language and add the compiled input dynamically to the program, or we need implement a rather complicated type-checker for the input. Both solutions are complicated and require a significant of work. Fortunately, Clean provides an advanced type-system for its dynamics. The existing type-system for these dynamic values can check all required type constraints. In this paper we show how we can make dynamic editors for complex user inputs in iTask programs using these dynamic types.

Abstract: In the light of algorithmic, as well as performance-related challenges in Eff-compilation, we introduce the implementation of an explicit type-and-effect system into the Eff-compiler, as described by Saleh et al. Thus, the way is cleared for a more efficient compilation to languages with a native effect system. We leverage this implementation to increase performance of compilation to languages without a native effect system as well. Karachalias et al. propose such a translation, which however does not seamlessly fit into the current state of the compiler. We describe the issues faced in integrating that translation, as well as a preliminary implementation.